Another example for eHoare (done with @mzini). This example considers a nested loop which uniformly samples a boolean matrix of size $n \times m$, and proves that the probably of sampling any boolean matrix of size $n \times m$ is no more than $2 ^ {- n \times m}$.

My original purpose for this example was to figure out a game hopping in a big proof, but it turned out that this game hopping is not needed. But I think this is a good example for demonstrating how to do proof in eHoare.